feat: Effective potential for Weyl fermions (Stacked on #1404) - #1415

…T Lagrangian

Fill all eleven remaining sorries in
Physlib/Particles/PureFermionic/EFTLagrangianExclDeriv.lean:

- coeff_fermionic_selection_rule: via termOfList_zero_of_not_nodup. The
  IsInvariant hypothesis is dropped: the rule holds for any potential.
- coeff_odd_selection_rule: fermion parity, via the new rep_neg_one_apply
  (the special case z = -1 of the diagonal family below).
- mem_allTermsWithIrrepContent_iff: via multisetsOfCard.
- eq_sum_irrepCoeff, eq_sum_massDimCoeff: via a new generic regrouping
  lemma eq_sum_fiber_coeff (decomposition of the support sum along any
  classifying map with specified fibers).
- irrepCoeff_rep, irrepCoeff_rep_apply_fieldSpecification: via
  rep_termOfList_eq_sum_of_toIrrep, through a shared monomial helper.
- irrepCoeff_ψ_barψ_eq_zero_of_isInvariant: no Lorentz-invariant operator
  mixes ψ with barψ. Proved with the new diagonal family
  diagSL (z : ℂˣ) : SL(2,ℂ) at z = 2i: the scaling factors of the four
  mixed pairs are 1/4, -1, -1 and 4, all ≠ 1, so
  coeff_U1_selection_rule applies. (Real diagonal elements, i.e. pure
  boosts, are insufficient: they scale the off-diagonal pairs by 1.)
  A TODO records that diagSL, diagSL_inv, diagSL_neg_one and twoI should
  move to Physlib.Relativity.SL2C.Basic when this development is split.

Repair the mass-dimension section, which did not compile:

- allTermsWithMassDimension is now the computable multisetsOfMassDim
  from the new file Physlib/Mathematics/MultisetsOfMassDim.lean
  (Finset.sym enumeration bounded by ⌊m / d_min⌋, with an ℕ-scaled
  decide-friendly variant and a denominator-clearing bridge lemma, as
  discussed on Zulip). upperBoundNumberOfFields is superseded by
  massDimCardBound.
- massDimCoeff is defined as a sum of coeff over this fixed finset, so
  linearity holds by construction (removing the map_add'/map_smul'
  sorries).
- decide examples: {ψ 0, ψ 1} has mass dimension 3; the quartic does not.

Also:

- fix the stale import Physlib.Particles.PureFermionic.EffectivePotential
  in Physlib.lean (renamed to EFTLagrangianExclDeriv), which broke the
  full-library build;
- add docstrings to all previously undocumented definitions;
- add simp evaluation lemmas so definitions stay opaque downstream
  (toIrrep_ψ, toIrrep_barψ, massDimension_eq, massDimensionNat_eq,
  diagSL_inv, diagSL_neg_one, diagScale_neg_one, diagScale_twoI_ψ,
  diagScale_twoI_barψ) and the structural fact sum_map_massDimension.

The changes passed a ten-angle rubric review (correctness, reuse, scope,
attribution, api-design, generality, placement, naming, documentation,
proof-quality); the review's requested changes (private bound lemmas,
authors header, defeq and simp-annotation hygiene, structure comments)
are incorporated, with the SL2C placement recorded as a TODO.

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…E.1 and E.2

…roofs

…n case

…ayer

Adds Physlib/ClassicalFieldTheory, a self-contained generalisation of the
jet-algebra machinery of the Standard Model to an arbitrary gauge group:

- JetAlgebra/: jets, jet component spaces, and the `IsFieldAlgebra` typeclass
  unifying bosonic (symmetric) and fermionic (exterior) field algebras, with
  jet derivatives, Lorentz, gauge and mass-weight actions.
- GaugeTheory/GaugeJet: the `GaugeJet` class of jets of a gauge group
  (evaluation, constants, derivative, adjoint, Maurer–Cartan form), with the
  Taylor–Leibniz and truncation extensions.
- GaugeTheory/GaugeBoson, GaugeField, Matter: gauge bosons valued in a Lie
  algebra, the `IsGaugeField` transformation law, covariant derivatives, and
  `MatterField` bundling the data of a matter field.

Supporting lemmas in Mathematics/MultisetAntidiagonal and the multiset basis
of DerivAlgebraReal. Two duplicate root-namespace declarations in the old
Standard Model files are dropped in favour of the generic ones.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017JtScjMeuHHQSbNfQxqhpx

…/JTSphyslib into AddPotentialAlgebra